Nuprl Lemma : grp_op_l
13,42
postcript
pdf
g
:GrpSig,
a
,
b
,
c
:|
g
|. (
b
=
c
)
((
a
*
b
) = (
a
*
c
)
|
g
|)
latex
Up
groups
1
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
f
y
Lemmas
grp
sig
wf
,
grp
car
wf
,
grp
op
wf
origin
g:GrpSig, a, b, c:|g|. (b = c) 
((a * b) = (a * c) 
|g|) g:GrpSig, a, b, c:|g|. (b = c) ((a * b) = (a * c) |g|) 
T Qx:A. B(x)